Nuprl Lemma : cond-to-list_wf
0,22
postcript
pdf
A
:Type,
x
:
A
+Unit. ?[
x
]
A
List
latex
Definitions
t
T
,
type
List
,
nil
,
car
.
cdr
,
left
+
right
,
?[
x
]
,
Type
,
Unit
,
x
:
A
.
B
(
x
)
Lemmas
unit
wf
origin
A:Type, x:A+Unit. ?[x] 
A List A:Type, x:A+Unit. ?[x] A List Tx:A. B(x)